/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Morgan Deters, Tim King
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Implementation of command objects.
 */

#include "parser/commands.h"

#include <exception>
#include <iostream>
#include <iterator>
#include <sstream>
#include <utility>
#include <vector>

#include "base/check.h"
#include "base/modal_exception.h"
#include "base/output.h"
#include "expr/node_manager.h"
#include "main/command_executor.h"
#include "options/io_utils.h"
#include "options/main_options.h"
#include "options/options.h"
#include "options/printer_options.h"
#include "options/smt_options.h"
#include "parser/command_status.h"
#include "parser/sym_manager.h"
#include "printer/printer.h"
#include "proof/unsat_core.h"
#include "util/smt2_quote_string.h"
#include "util/utility.h"

using namespace std;

namespace cvc5::parser {

std::string sexprToString(cvc5::Term sexpr)
{
  // if sexpr has a symbol, return its symbol. We don't
  // call Term::toString as its result depends on the output language.
  // Notice that we only check for terms with symbols. The sexprs generated by
  // the parser don't contains other atomic terms, so we can ignore them.
  if (sexpr.hasSymbol())
  {
    return sexpr.getSymbol();
  }

  // if sexpr is not a spec constant, make sure it is an array of sub-sexprs
  Assert(sexpr.getKind() == cvc5::Kind::SEXPR);

  std::stringstream ss;
  auto it = sexpr.begin();

  // recursively print the sub-sexprs
  ss << '(' << sexprToString(*it);
  ++it;
  while (it != sexpr.end())
  {
    ss << ' ' << sexprToString(*it);
    ++it;
  }
  ss << ')';

  return ss.str();
}

/* -------------------------------------------------------------------------- */
/* Cmd                                                                        */
/* -------------------------------------------------------------------------- */

Cmd::Cmd() : d_commandStatus(nullptr) {}

Cmd::Cmd(const Cmd& cmd)
{
  d_commandStatus = (cmd.d_commandStatus == nullptr)
                        ? nullptr
                        : &cmd.d_commandStatus->clone();
}

Cmd::~Cmd()
{
  if (d_commandStatus != nullptr
      && d_commandStatus != CommandSuccess::instance())
  {
    delete d_commandStatus;
  }
}

bool Cmd::ok() const
{
  // either we haven't run the command yet, or it ran successfully
  return d_commandStatus == nullptr
         || dynamic_cast<const CommandSuccess*>(d_commandStatus) != nullptr;
}

bool Cmd::fail() const
{
  return d_commandStatus != nullptr
         && dynamic_cast<const CommandFailure*>(d_commandStatus) != nullptr;
}

bool Cmd::interrupted() const
{
  return d_commandStatus != nullptr
         && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != nullptr;
}

void Cmd::invoke(cvc5::Solver* solver,
                 parser::SymManager* sm,
                 std::ostream& out)
{
  invoke(solver, sm);
  if (!ok())
  {
    out << *d_commandStatus;
  }
  else
  {
    printResult(solver, out);
  }
  // always flush the output
  out << std::flush;
}

std::string Cmd::toString() const
{
  std::stringstream ss;
  toStream(ss);
  return ss.str();
}

void Cmd::printResult(cvc5::Solver* solver, std::ostream& out) const
{
  if (!ok()
      || (d_commandStatus != nullptr
          && solver->getOption("print-success") == "true"))
  {
    out << *d_commandStatus;
  }
}

void Cmd::resetSolver(cvc5::Solver* solver)
{
  std::unique_ptr<internal::Options> opts =
      std::make_unique<internal::Options>();
  opts->copyValues(*solver->d_originalOptions);
  // This reconstructs a new solver object at the same memory location as the
  // current one. Note that this command does not own the solver object!
  // It may be safer to instead make the ResetCommand a special case in the
  // CommandExecutor such that this reconstruction can be done within the
  // CommandExecutor, who actually owns the solver.
  TermManager& tm = solver->getTermManager();
  solver->~Solver();
  new (solver) cvc5::Solver(tm, std::move(opts));
}

internal::Node Cmd::termToNode(const cvc5::Term& term)
{
  return term.getNode();
}

std::vector<internal::Node> Cmd::termVectorToNodes(
    const std::vector<cvc5::Term>& terms)
{
  return cvc5::Term::termVectorToNodes(terms);
}

internal::TypeNode Cmd::sortToTypeNode(const cvc5::Sort& sort)
{
  return sort.getTypeNode();
}

std::vector<internal::TypeNode> Cmd::sortVectorToTypeNodes(
    const std::vector<cvc5::Sort>& sorts)
{
  return cvc5::Sort::sortVectorToTypeNodes(sorts);
}

internal::TypeNode Cmd::grammarToTypeNode(cvc5::Grammar* grammar)
{
  return grammar == nullptr ? internal::TypeNode::null()
                            : sortToTypeNode(grammar->resolve());
}

std::ostream& operator<<(std::ostream& out, const Cmd& c)
{
  out << c.toString();
  return out;
}

std::ostream& operator<<(std::ostream& out, const Cmd* c)
{
  if (c == nullptr)
  {
    out << "null";
  }
  else
  {
    out << *c;
  }
  return out;
}

/* -------------------------------------------------------------------------- */
/* class EmptyCommand                                                         */
/* -------------------------------------------------------------------------- */

EmptyCommand::EmptyCommand(std::string name) : d_name(name) {}
std::string EmptyCommand::getName() const { return d_name; }
void EmptyCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  /* empty commands have no implementation */
  d_commandStatus = CommandSuccess::instance();
}

std::string EmptyCommand::getCommandName() const { return "empty"; }

void EmptyCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdEmpty(out, d_name);
}

/* -------------------------------------------------------------------------- */
/* class EchoCommand                                                          */
/* -------------------------------------------------------------------------- */

EchoCommand::EchoCommand(std::string output) : d_output(output) {}

std::string EchoCommand::getOutput() const { return d_output; }

void EchoCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  d_commandStatus = CommandSuccess::instance();
}

void EchoCommand::printResult(cvc5::Solver* solver, std::ostream& out) const
{
  Trace("dtview::command") << "* ~COMMAND: echo |" << d_output << "|~"
                           << std::endl;
  out << cvc5::internal::quoteString(d_output) << std::endl;
}

std::string EchoCommand::getCommandName() const { return "echo"; }

void EchoCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdEcho(out, d_output);
}

/* -------------------------------------------------------------------------- */
/* class AssertCommand                                                        */
/* -------------------------------------------------------------------------- */

AssertCommand::AssertCommand(const cvc5::Term& t) : d_term(t) {}

cvc5::Term AssertCommand::getTerm() const { return d_term; }
void AssertCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    solver->assertFormula(d_term);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

std::string AssertCommand::getCommandName() const { return "assert"; }

void AssertCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdAssert(out,
                                                        termToNode(d_term));
}

/* -------------------------------------------------------------------------- */
/* class PushCommand                                                          */
/* -------------------------------------------------------------------------- */

PushCommand::PushCommand(uint32_t nscopes) : d_nscopes(nscopes) {}

void PushCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    solver->push(d_nscopes);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

std::string PushCommand::getCommandName() const { return "push"; }

void PushCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdPush(out, d_nscopes);
}

/* -------------------------------------------------------------------------- */
/* class PopCommand                                                           */
/* -------------------------------------------------------------------------- */

PopCommand::PopCommand(uint32_t nscopes) : d_nscopes(nscopes) {}

void PopCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    solver->pop(d_nscopes);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

std::string PopCommand::getCommandName() const { return "pop"; }

void PopCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdPop(out, d_nscopes);
}

/* -------------------------------------------------------------------------- */
/* class CheckSatCommand                                                      */
/* -------------------------------------------------------------------------- */

CheckSatCommand::CheckSatCommand() {}

void CheckSatCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  Trace("dtview::command") << "* ~COMMAND: " << getCommandName() << "~"
                           << std::endl;
  try
  {
    d_result = solver->checkSat();
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

cvc5::Result CheckSatCommand::getResult() const { return d_result; }

void CheckSatCommand::printResult(cvc5::Solver* solver, std::ostream& out) const
{
  out << d_result << endl;
}

std::string CheckSatCommand::getCommandName() const { return "check-sat"; }

void CheckSatCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdCheckSat(out);
}

/* -------------------------------------------------------------------------- */
/* class CheckSatAssumingCommand                                              */
/* -------------------------------------------------------------------------- */

CheckSatAssumingCommand::CheckSatAssumingCommand(cvc5::Term term)
    : d_terms({term})
{
}

CheckSatAssumingCommand::CheckSatAssumingCommand(
    const std::vector<cvc5::Term>& terms)
    : d_terms(terms)
{
}

const std::vector<cvc5::Term>& CheckSatAssumingCommand::getTerms() const
{
  return d_terms;
}

void CheckSatAssumingCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  Trace("dtview::command") << "* ~COMMAND: (check-sat-assuming ( " << d_terms
                           << " )~" << std::endl;
  try
  {
    d_result = solver->checkSatAssuming(d_terms);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

cvc5::Result CheckSatAssumingCommand::getResult() const
{
  Trace("dtview::command") << "* ~RESULT: " << d_result << "~" << std::endl;
  return d_result;
}

void CheckSatAssumingCommand::printResult(cvc5::Solver* solver,
                                          std::ostream& out) const
{
  out << d_result << endl;
}

std::string CheckSatAssumingCommand::getCommandName() const
{
  return "check-sat-assuming";
}

void CheckSatAssumingCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdCheckSatAssuming(
      out, termVectorToNodes(d_terms));
}

/* -------------------------------------------------------------------------- */
/* class DeclareSygusVarCommand */
/* -------------------------------------------------------------------------- */

DeclareSygusVarCommand::DeclareSygusVarCommand(const std::string& id,
                                               cvc5::Sort sort)
    : DeclarationDefinitionCommand(id), d_sort(sort)
{
}

cvc5::Sort DeclareSygusVarCommand::getSort() const { return d_sort; }

void DeclareSygusVarCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  Term var = solver->declareSygusVar(d_symbol, d_sort);
  if (!bindToTerm(sm, var, true))
  {
    return;
  }
  d_commandStatus = CommandSuccess::instance();
}

std::string DeclareSygusVarCommand::getCommandName() const
{
  return "declare-var";
}

void DeclareSygusVarCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdDeclareVar(
      out, d_symbol, sortToTypeNode(d_sort));
}

/* -------------------------------------------------------------------------- */
/* class SynthFunCommand                                                      */
/* -------------------------------------------------------------------------- */

SynthFunCommand::SynthFunCommand(const std::string& id,
                                 const std::vector<cvc5::Term>& vars,
                                 cvc5::Sort sort,
                                 cvc5::Grammar* g)
    : DeclarationDefinitionCommand(id), d_vars(vars), d_sort(sort), d_grammar(g)
{
}

const std::vector<cvc5::Term>& SynthFunCommand::getVars() const
{
  return d_vars;
}

cvc5::Sort SynthFunCommand::getSort() const { return d_sort; }

const cvc5::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; }

void SynthFunCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  Term fun;
  if (d_grammar != nullptr)
  {
    fun = solver->synthFun(d_symbol, d_vars, d_sort, *d_grammar);
  }
  else
  {
    fun = solver->synthFun(d_symbol, d_vars, d_sort);
  }
  if (!bindToTerm(sm, fun, true))
  {
    return;
  }
  sm->addFunctionToSynthesize(fun);
  d_commandStatus = CommandSuccess::instance();
}

std::string SynthFunCommand::getCommandName() const { return "synth-fun"; }

void SynthFunCommand::toStream(std::ostream& out) const
{
  std::vector<internal::Node> nodeVars = termVectorToNodes(d_vars);
  internal::Printer::getPrinter(out)->toStreamCmdSynthFun(
      out,
      d_symbol,
      nodeVars,
      sortToTypeNode(d_sort),
      d_grammar == nullptr ? internal::TypeNode::null()
                           : grammarToTypeNode(d_grammar));
}

/* -------------------------------------------------------------------------- */
/* class SygusConstraintCommand */
/* -------------------------------------------------------------------------- */

SygusConstraintCommand::SygusConstraintCommand(const cvc5::Term& t,
                                               bool isAssume)
    : d_term(t), d_isAssume(isAssume)
{
}

void SygusConstraintCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    if (d_isAssume)
    {
      solver->addSygusAssume(d_term);
    }
    else
    {
      solver->addSygusConstraint(d_term);
    }
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

cvc5::Term SygusConstraintCommand::getTerm() const { return d_term; }

std::string SygusConstraintCommand::getCommandName() const
{
  return d_isAssume ? "assume" : "constraint";
}

void SygusConstraintCommand::toStream(std::ostream& out) const
{
  if (d_isAssume)
  {
    internal::Printer::getPrinter(out)->toStreamCmdAssume(out,
                                                          termToNode(d_term));
  }
  else
  {
    internal::Printer::getPrinter(out)->toStreamCmdConstraint(
        out, termToNode(d_term));
  }
}

/* -------------------------------------------------------------------------- */
/* class SygusInvConstraintCommand */
/* -------------------------------------------------------------------------- */

SygusInvConstraintCommand::SygusInvConstraintCommand(
    const std::vector<cvc5::Term>& predicates)
    : d_predicates(predicates)
{
}

SygusInvConstraintCommand::SygusInvConstraintCommand(const cvc5::Term& inv,
                                                     const cvc5::Term& pre,
                                                     const cvc5::Term& trans,
                                                     const cvc5::Term& post)
    : SygusInvConstraintCommand(std::vector<cvc5::Term>{inv, pre, trans, post})
{
}

void SygusInvConstraintCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    solver->addSygusInvConstraint(
        d_predicates[0], d_predicates[1], d_predicates[2], d_predicates[3]);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

const std::vector<cvc5::Term>& SygusInvConstraintCommand::getPredicates() const
{
  return d_predicates;
}

std::string SygusInvConstraintCommand::getCommandName() const
{
  return "inv-constraint";
}

void SygusInvConstraintCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdInvConstraint(
      out,
      termToNode(d_predicates[0]),
      termToNode(d_predicates[1]),
      termToNode(d_predicates[2]),
      termToNode(d_predicates[3]));
}

/* -------------------------------------------------------------------------- */
/* class CheckSynthCommand                                                    */
/* -------------------------------------------------------------------------- */

void CheckSynthCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    d_result = d_isNext ? solver->checkSynthNext() : solver->checkSynth();
    d_commandStatus = CommandSuccess::instance();
    d_solution.clear();
    // check whether we should print the status
    std::string sygusOut = solver->getOption("sygus-out");
    if (!d_result.hasSolution() || sygusOut == "status-and-def"
        || sygusOut == "status")
    {
      if (d_result.hasSolution())
      {
        d_solution << "feasible" << std::endl;
      }
      else if (d_result.hasNoSolution())
      {
        d_solution << "infeasible" << std::endl;
      }
      else
      {
        d_solution << "fail" << std::endl;
      }
    }
    // check whether we should print the solution
    if (d_result.hasSolution() && sygusOut != "status")
    {
      std::vector<cvc5::Term> synthFuns = sm->getFunctionsToSynthesize();
      d_solution << "(" << std::endl;
      internal::options::ioutils::Scope scope(d_solution);
      internal::options::ioutils::applyOutputLanguage(
          d_solution, internal::Language::LANG_SYGUS_V2);
      internal::Printer* p = internal::Printer::getPrinter(d_solution);
      for (cvc5::Term& f : synthFuns)
      {
        cvc5::Term sol = solver->getSynthSolution(f);
        std::vector<cvc5::Term> formals;
        if (sol.getKind() == cvc5::Kind::LAMBDA)
        {
          formals.insert(formals.end(), sol[0].begin(), sol[0].end());
          sol = sol[1];
        }
        cvc5::Sort rangeSort = f.getSort();
        if (rangeSort.isFunction())
        {
          rangeSort = rangeSort.getFunctionCodomainSort();
        }
        p->toStreamCmdDefineFunction(d_solution,
                                     f.toString(),
                                     termVectorToNodes(formals),
                                     sortToTypeNode(rangeSort),
                                     termToNode(sol));
        d_solution << std::endl;
      }
      d_solution << ")" << std::endl;
    }
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

cvc5::SynthResult CheckSynthCommand::getResult() const { return d_result; }
void CheckSynthCommand::printResult(cvc5::Solver* solver,
                                    std::ostream& out) const
{
  out << d_solution.str();
}

std::string CheckSynthCommand::getCommandName() const
{
  return d_isNext ? "check-synth-next" : "check-synth";
}

void CheckSynthCommand::toStream(std::ostream& out) const
{
  if (d_isNext)
  {
    internal::Printer::getPrinter(out)->toStreamCmdCheckSynthNext(out);
  }
  else
  {
    internal::Printer::getPrinter(out)->toStreamCmdCheckSynth(out);
  }
}

/* -------------------------------------------------------------------------- */
/* class FindSynthCommand                                                    */
/* -------------------------------------------------------------------------- */

void FindSynthCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    if (d_grammar != nullptr)
    {
      d_result = solver->findSynth(d_fst, *d_grammar);
    }
    else
    {
      d_result = solver->findSynth(d_fst);
    }
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

Term FindSynthCommand::getResult() const { return d_result; }
void FindSynthCommand::printResult(cvc5::Solver* solver,
                                   std::ostream& out) const
{
  if (d_result.isNull())
  {
    out << "fail" << std::endl;
  }
  else
  {
    out << d_result << std::endl;
  }
}

std::string FindSynthCommand::getCommandName() const { return "find-synth"; }

void FindSynthCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdFindSynth(
      out,
      d_fst,
      d_grammar == nullptr ? internal::TypeNode::null()
                           : grammarToTypeNode(d_grammar));
}

/* -------------------------------------------------------------------------- */
/* class FindSynthNextCommand */
/* -------------------------------------------------------------------------- */

cvc5::Term FindSynthNextCommand::getResult() const { return d_result; }

void FindSynthNextCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    // Get the name of the abduct from the symbol manager
    d_result = solver->findSynthNext();
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

void FindSynthNextCommand::printResult(cvc5::Solver* solver,
                                       std::ostream& out) const
{
  if (d_result.isNull())
  {
    out << "fail" << std::endl;
  }
  else
  {
    out << d_result << std::endl;
  }
}

std::string FindSynthNextCommand::getCommandName() const
{
  return "find-synth-next";
}

void FindSynthNextCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdFindSynthNext(out);
}

/* -------------------------------------------------------------------------- */
/* class ResetCommand                                                         */
/* -------------------------------------------------------------------------- */

void ResetCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    sm->reset();
    resetSolver(solver);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

std::string ResetCommand::getCommandName() const { return "reset"; }

void ResetCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdReset(out);
}

/* -------------------------------------------------------------------------- */
/* class ResetAssertionsCommand                                               */
/* -------------------------------------------------------------------------- */

void ResetAssertionsCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    sm->resetAssertions();
    solver->resetAssertions();
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

std::string ResetAssertionsCommand::getCommandName() const
{
  return "reset-assertions";
}

void ResetAssertionsCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdResetAssertions(out);
}

/* -------------------------------------------------------------------------- */
/* class QuitCommand                                                          */
/* -------------------------------------------------------------------------- */

void QuitCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  d_commandStatus = CommandSuccess::instance();
}

std::string QuitCommand::getCommandName() const { return "exit"; }

void QuitCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdQuit(out);
}

/* -------------------------------------------------------------------------- */
/* class DeclarationDefinitionCommand                                         */
/* -------------------------------------------------------------------------- */

DeclarationDefinitionCommand::DeclarationDefinitionCommand(
    const std::string& id)
    : d_symbol(id)
{
}

std::string DeclarationDefinitionCommand::getSymbol() const { return d_symbol; }

bool tryBindToTerm(SymManager* sm,
                   const std::string& sym,
                   Term t,
                   bool doOverload,
                   std::ostream* out = nullptr)
{
  if (!sm->bind(sym, t, true))
  {
    if (out)
    {
      (*out) << "Cannot bind " << sym << " to symbol of type " << t.getSort();
      (*out) << ", maybe the symbol has already been defined?";
    }
    return false;
  }
  return true;
}

bool DeclarationDefinitionCommand::bindToTerm(SymManager* sm,
                                              Term t,
                                              bool doOverload)
{
  if (!tryBindToTerm(sm, d_symbol, t, doOverload))
  {
    std::stringstream ss;
    tryBindToTerm(sm, d_symbol, t, doOverload, &ss);
    d_commandStatus = new CommandFailure(ss.str());
    return false;
  }
  return true;
}

/* -------------------------------------------------------------------------- */
/* class DeclareFunctionCommand                                               */
/* -------------------------------------------------------------------------- */

DeclareFunctionCommand::DeclareFunctionCommand(
    const std::string& id, const std::vector<Sort>& argSorts, cvc5::Sort sort)
    : DeclarationDefinitionCommand(id), d_argSorts(argSorts), d_sort(sort)
{
}
std::vector<Sort> DeclareFunctionCommand::getArgSorts() const
{
  return d_argSorts;
}
cvc5::Sort DeclareFunctionCommand::getSort() const { return d_sort; }

void DeclareFunctionCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  // determine if this will be a fresh declaration
  bool fresh = sm->getFreshDeclarations();
  Term fun = solver->declareFun(d_symbol, d_argSorts, d_sort, fresh);
  if (!bindToTerm(sm, fun, true))
  {
    return;
  }
  // mark that it will be printed in the model
  sm->addModelDeclarationTerm(fun);
  d_commandStatus = CommandSuccess::instance();
}

std::string DeclareFunctionCommand::getCommandName() const
{
  return "declare-fun";
}

void DeclareFunctionCommand::toStream(std::ostream& out) const
{
  // Note we use the symbol of the function here. This makes a difference
  // in the rare case we are binding a symbol in the parser to a variable
  // whose name is different. For example, when converting TPTP to smt2,
  // we require a namespace prefix. Using the function symbol name ensures
  // that e.g. `-o raw-benchmark` results in a valid benchmark.
  internal::Printer::getPrinter(out)->toStreamCmdDeclareFunction(
      out, d_symbol, sortVectorToTypeNodes(d_argSorts), sortToTypeNode(d_sort));
}

/* -------------------------------------------------------------------------- */
/* class DeclarePoolCommand                                               */
/* -------------------------------------------------------------------------- */

DeclarePoolCommand::DeclarePoolCommand(const std::string& id,
                                       cvc5::Sort sort,
                                       const std::vector<cvc5::Term>& initValue)
    : DeclarationDefinitionCommand(id), d_sort(sort), d_initValue(initValue)
{
}

cvc5::Sort DeclarePoolCommand::getSort() const { return d_sort; }
const std::vector<cvc5::Term>& DeclarePoolCommand::getInitialValue() const
{
  return d_initValue;
}

void DeclarePoolCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  Term pool = solver->declarePool(d_symbol, d_sort, d_initValue);
  if (!bindToTerm(sm, pool, true))
  {
    return;
  }
  // Notice that the pool is already declared by the parser so that it the
  // symbol is bound eagerly. This is analogous to DeclareSygusVarCommand.
  // Hence, we do nothing here.
  d_commandStatus = CommandSuccess::instance();
}

std::string DeclarePoolCommand::getCommandName() const
{
  return "declare-pool";
}

void DeclarePoolCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdDeclarePool(
      out, d_symbol, sortToTypeNode(d_sort), termVectorToNodes(d_initValue));
}

/* -------------------------------------------------------------------------- */
/* class DeclareOracleFunCommand */
/* -------------------------------------------------------------------------- */

DeclareOracleFunCommand::DeclareOracleFunCommand(
    const std::string& id, const std::vector<Sort>& argSorts, Sort sort)
    : d_id(id), d_argSorts(argSorts), d_sort(sort), d_binName("")
{
}
DeclareOracleFunCommand::DeclareOracleFunCommand(
    const std::string& id,
    const std::vector<Sort>& argSorts,
    Sort sort,
    const std::string& binName)
    : d_id(id), d_argSorts(argSorts), d_sort(sort), d_binName(binName)
{
}

const std::string& DeclareOracleFunCommand::getIdentifier() const
{
  return d_id;
}

Sort DeclareOracleFunCommand::getSort() const { return d_sort; }

const std::string& DeclareOracleFunCommand::getBinaryName() const
{
  return d_binName;
}

void DeclareOracleFunCommand::invoke(Solver* solver, SymManager* sm)
{
  std::vector<Sort> args;
  Sort ret;
  if (d_sort.isFunction())
  {
    args = d_sort.getFunctionDomainSorts();
    ret = d_sort.getFunctionCodomainSort();
  }
  else
  {
    ret = d_sort;
  }
  // will call solver declare oracle function when available in API
  d_commandStatus = CommandSuccess::instance();
}

std::string DeclareOracleFunCommand::getCommandName() const
{
  return "declare-oracle-fun";
}

void DeclareOracleFunCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdDeclareOracleFun(
      out,
      d_id,
      sortVectorToTypeNodes(d_argSorts),
      sortToTypeNode(d_sort),
      d_binName);
}

/* -------------------------------------------------------------------------- */
/* class DeclareSortCommand                                                   */
/* -------------------------------------------------------------------------- */

DeclareSortCommand::DeclareSortCommand(const std::string& id, size_t arity)
    : DeclarationDefinitionCommand(id), d_arity(arity)
{
}

size_t DeclareSortCommand::getArity() const { return d_arity; }
void DeclareSortCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  // determine if this will be a fresh declaration
  bool fresh = sm->getFreshDeclarations();
  Sort sort = solver->declareSort(d_symbol, d_arity, fresh);
  sm->bindType(d_symbol, std::vector<Sort>(d_arity), sort);
  // mark that it will be printed in the model, if it is an uninterpreted
  // sort (arity 0)
  if (d_arity == 0)
  {
    sm->addModelDeclarationSort(sort);
  }
  d_commandStatus = CommandSuccess::instance();
}

std::string DeclareSortCommand::getCommandName() const
{
  return "declare-sort";
}

void DeclareSortCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdDeclareType(
      out, d_symbol, d_arity);
}

/* -------------------------------------------------------------------------- */
/* class DefineSortCommand                                                    */
/* -------------------------------------------------------------------------- */

DefineSortCommand::DefineSortCommand(const std::string& id, cvc5::Sort sort)
    : DeclarationDefinitionCommand(id), d_params(), d_sort(sort)
{
}

DefineSortCommand::DefineSortCommand(const std::string& id,
                                     const std::vector<cvc5::Sort>& params,
                                     cvc5::Sort sort)
    : DeclarationDefinitionCommand(id), d_params(params), d_sort(sort)
{
}

const std::vector<cvc5::Sort>& DefineSortCommand::getParameters() const
{
  return d_params;
}

cvc5::Sort DefineSortCommand::getSort() const { return d_sort; }
void DefineSortCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  // This name is not its own distinct sort, it's an alias.
  sm->bindType(d_symbol, d_params, d_sort);
  d_commandStatus = CommandSuccess::instance();
}

std::string DefineSortCommand::getCommandName() const { return "define-sort"; }

void DefineSortCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdDefineType(
      out, d_symbol, sortVectorToTypeNodes(d_params), sortToTypeNode(d_sort));
}

/* -------------------------------------------------------------------------- */
/* class DefineFunctionCommand                                                */
/* -------------------------------------------------------------------------- */

DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
                                             cvc5::Sort sort,
                                             cvc5::Term formula)
    : DeclarationDefinitionCommand(id),
      d_formals(),
      d_sort(sort),
      d_formula(formula)
{
}

DefineFunctionCommand::DefineFunctionCommand(
    const std::string& id,
    const std::vector<cvc5::Term>& formals,
    cvc5::Sort sort,
    cvc5::Term formula)
    : DeclarationDefinitionCommand(id),
      d_formals(formals),
      d_sort(sort),
      d_formula(formula)
{
}

const std::vector<cvc5::Term>& DefineFunctionCommand::getFormals() const
{
  return d_formals;
}

cvc5::Sort DefineFunctionCommand::getSort() const { return d_sort; }

cvc5::Term DefineFunctionCommand::getFormula() const { return d_formula; }

void DefineFunctionCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    bool global = sm->getGlobalDeclarations();
    cvc5::Term fun =
        solver->defineFun(d_symbol, d_formals, d_sort, d_formula, global);
    if (!bindToTerm(sm, fun, true))
    {
      return;
    }
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

std::string DefineFunctionCommand::getCommandName() const
{
  return "define-fun";
}

void DefineFunctionCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdDefineFunction(
      out,
      d_symbol,
      termVectorToNodes(d_formals),
      sortToTypeNode(d_sort),
      termToNode(d_formula));
}

/* -------------------------------------------------------------------------- */
/* class DefineFunctionRecCommand                                             */
/* -------------------------------------------------------------------------- */

DefineFunctionRecCommand::DefineFunctionRecCommand(
    cvc5::Term func, const std::vector<cvc5::Term>& formals, cvc5::Term formula)
{
  d_funcs.push_back(func);
  d_formals.push_back(formals);
  d_formulas.push_back(formula);
}

DefineFunctionRecCommand::DefineFunctionRecCommand(
    const std::vector<cvc5::Term>& funcs,
    const std::vector<std::vector<cvc5::Term>>& formals,
    const std::vector<cvc5::Term>& formulas)
    : d_funcs(funcs), d_formals(formals), d_formulas(formulas)
{
}

const std::vector<cvc5::Term>& DefineFunctionRecCommand::getFunctions() const
{
  return d_funcs;
}

const std::vector<std::vector<cvc5::Term>>&
DefineFunctionRecCommand::getFormals() const
{
  return d_formals;
}

const std::vector<cvc5::Term>& DefineFunctionRecCommand::getFormulas() const
{
  return d_formulas;
}

void DefineFunctionRecCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    // bind each, returning if failure if we fail to bind
    for (const Term& f : d_funcs)
    {
      Assert(f.hasSymbol());
      const std::string s = f.getSymbol();
      if (!tryBindToTerm(sm, s, f, true))
      {
        std::stringstream ss;
        tryBindToTerm(sm, s, f, true, &ss);
        d_commandStatus = new CommandFailure(ss.str());
        return;
      }
    }
    bool global = sm->getGlobalDeclarations();
    solver->defineFunsRec(d_funcs, d_formals, d_formulas, global);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

std::string DefineFunctionRecCommand::getCommandName() const
{
  return "define-fun-rec";
}

void DefineFunctionRecCommand::toStream(std::ostream& out) const
{
  std::vector<std::vector<internal::Node>> formals;
  formals.reserve(d_formals.size());
  for (const std::vector<cvc5::Term>& formal : d_formals)
  {
    formals.push_back(termVectorToNodes(formal));
  }

  internal::Printer::getPrinter(out)->toStreamCmdDefineFunctionRec(
      out, termVectorToNodes(d_funcs), formals, termVectorToNodes(d_formulas));
}
/* -------------------------------------------------------------------------- */
/* class DeclareHeapCommand                                                   */
/* -------------------------------------------------------------------------- */
DeclareHeapCommand::DeclareHeapCommand(cvc5::Sort locSort, cvc5::Sort dataSort)
    : d_locSort(locSort), d_dataSort(dataSort)
{
}

cvc5::Sort DeclareHeapCommand::getLocationSort() const { return d_locSort; }
cvc5::Sort DeclareHeapCommand::getDataSort() const { return d_dataSort; }

void DeclareHeapCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  solver->declareSepHeap(d_locSort, d_dataSort);
}

std::string DeclareHeapCommand::getCommandName() const
{
  return "declare-heap";
}

void DeclareHeapCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdDeclareHeap(
      out, sortToTypeNode(d_locSort), sortToTypeNode(d_dataSort));
}

/* -------------------------------------------------------------------------- */
/* class SimplifyCommand                                                      */
/* -------------------------------------------------------------------------- */

SimplifyCommand::SimplifyCommand(cvc5::Term term) : d_term(term) {}
cvc5::Term SimplifyCommand::getTerm() const { return d_term; }
void SimplifyCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    d_result = solver->simplify(d_term);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

cvc5::Term SimplifyCommand::getResult() const { return d_result; }
void SimplifyCommand::printResult(cvc5::Solver* solver, std::ostream& out) const
{
  out << d_result << endl;
}

std::string SimplifyCommand::getCommandName() const { return "simplify"; }

void SimplifyCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdSimplify(out,
                                                          termToNode(d_term));
}

/* -------------------------------------------------------------------------- */
/* class GetValueCommand                                                      */
/* -------------------------------------------------------------------------- */

GetValueCommand::GetValueCommand(cvc5::Term term) : d_terms()
{
  d_terms.push_back(term);
}

GetValueCommand::GetValueCommand(const std::vector<cvc5::Term>& terms)
    : d_terms(terms)
{
  Assert(terms.size() >= 1) << "cannot get-value of an empty set of terms";
}

const std::vector<cvc5::Term>& GetValueCommand::getTerms() const
{
  return d_terms;
}
void GetValueCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    d_result = solver->getValue(d_terms);
    Assert(d_result.size() == d_terms.size());
    d_commandStatus = CommandSuccess::instance();
  }
  catch (cvc5::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.what());
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

const std::vector<cvc5::Term>& GetValueCommand::getResult() const
{
  return d_result;
}
void GetValueCommand::printResult(cvc5::Solver* solver, std::ostream& out) const
{
  Assert(d_result.size() == d_terms.size());
  // we print each of the values separately since we do not want
  // to letify across key/value pairs in this list.
  out << "(";
  bool firstTime = true;
  for (size_t i = 0, rsize = d_result.size(); i < rsize; i++)
  {
    if (firstTime)
    {
      firstTime = false;
    }
    else
    {
      out << " ";
    }
    out << "(" << d_terms[i] << " " << d_result[i] << ")";
  }
  out << ")" << std::endl;
}

std::string GetValueCommand::getCommandName() const { return "get-value"; }

void GetValueCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdGetValue(
      out, termVectorToNodes(d_terms));
}

/* -------------------------------------------------------------------------- */
/* class GetAssignmentCommand                                                 */
/* -------------------------------------------------------------------------- */

GetAssignmentCommand::GetAssignmentCommand() {}
void GetAssignmentCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    TermManager& tm = solver->getTermManager();
    std::map<cvc5::Term, std::string> enames = sm->getExpressionNames();
    std::vector<cvc5::Term> terms;
    std::vector<std::string> names;
    for (const std::pair<const cvc5::Term, std::string>& e : enames)
    {
      terms.push_back(e.first);
      names.push_back(e.second);
    }
    // Must use vector version of getValue to ensure error is thrown regardless
    // of whether terms is empty.
    std::vector<cvc5::Term> values = solver->getValue(terms);
    Assert(values.size() == names.size());
    std::vector<cvc5::Term> sexprs;
    for (size_t i = 0, nterms = terms.size(); i < nterms; i++)
    {
      // Treat the expression name as a variable name as opposed to a string
      // constant to avoid printing double quotes around the name.
      cvc5::Term name = tm.mkVar(tm.getBooleanSort(), names[i]);
      sexprs.push_back(tm.mkTerm(cvc5::Kind::SEXPR, {name, values[i]}));
    }
    d_result = tm.mkTerm(cvc5::Kind::SEXPR, sexprs);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (cvc5::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.what());
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

cvc5::Term GetAssignmentCommand::getResult() const { return d_result; }
void GetAssignmentCommand::printResult(cvc5::Solver* solver,
                                       std::ostream& out) const
{
  out << d_result << endl;
}

std::string GetAssignmentCommand::getCommandName() const
{
  return "get-assignment";
}

void GetAssignmentCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdGetAssignment(out);
}

/* -------------------------------------------------------------------------- */
/* class GetModelCommand                                                      */
/* -------------------------------------------------------------------------- */

GetModelCommand::GetModelCommand() {}
void GetModelCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    std::vector<cvc5::Sort> declareSorts = sm->getDeclaredSorts();
    std::vector<cvc5::Term> declareTerms = sm->getDeclaredTerms();
    d_result = solver->getModel(declareSorts, declareTerms);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (cvc5::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.what());
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

void GetModelCommand::printResult(cvc5::Solver* solver, std::ostream& out) const
{
  out << d_result;
}

std::string GetModelCommand::getCommandName() const { return "get-model"; }

void GetModelCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdGetModel(out);
}

/* -------------------------------------------------------------------------- */
/* class BlockModelCommand */
/* -------------------------------------------------------------------------- */

BlockModelCommand::BlockModelCommand(modes::BlockModelsMode mode) : d_mode(mode)
{
}
void BlockModelCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    solver->blockModel(d_mode);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (cvc5::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.what());
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

std::string BlockModelCommand::getCommandName() const { return "block-model"; }

void BlockModelCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdBlockModel(out, d_mode);
}

/* -------------------------------------------------------------------------- */
/* class BlockModelValuesCommand */
/* -------------------------------------------------------------------------- */

BlockModelValuesCommand::BlockModelValuesCommand(
    const std::vector<cvc5::Term>& terms)
    : d_terms(terms)
{
  Assert(terms.size() >= 1)
      << "cannot block-model-values of an empty set of terms";
}

const std::vector<cvc5::Term>& BlockModelValuesCommand::getTerms() const
{
  return d_terms;
}
void BlockModelValuesCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    solver->blockModelValues(d_terms);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (cvc5::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.what());
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

std::string BlockModelValuesCommand::getCommandName() const
{
  return "block-model-values";
}

void BlockModelValuesCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdBlockModelValues(
      out, termVectorToNodes(d_terms));
}

/* -------------------------------------------------------------------------- */
/* class GetProofCommand                                                      */
/* -------------------------------------------------------------------------- */

GetProofCommand::GetProofCommand(modes::ProofComponent c) : d_component(c) {}
void GetProofCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    stringstream ss;
    const vector<cvc5::Proof> ps = solver->getProof(d_component);

    bool commentProves = !(d_component == modes::ProofComponent::SAT
                           || d_component == modes::ProofComponent::FULL);
    modes::ProofFormat format = modes::ProofFormat::DEFAULT;
    // Ignore proof format, if the proof is not the full proof
    if (d_component != modes::ProofComponent::FULL)
    {
      format = modes::ProofFormat::NONE;
    }

    if (format == modes::ProofFormat::NONE)
    {
      ss << "(" << std::endl;
    }
    for (Proof p : ps)
    {
      if (commentProves)
      {
        ss << "(!" << std::endl;
      }
      // get assertions, and build a map between them and their names
      std::map<cvc5::Term, std::string> assertionNames =
          sm->getExpressionNames(true);
      ss << solver->proofToString(p, format, assertionNames);
      if (commentProves)
      {
        ss << ":proves " << p.getResult() << ")" << std::endl;
      }
    }
    if (format == modes::ProofFormat::NONE)
    {
      ss << ")" << std::endl;
    }
    d_result = ss.str();
    d_commandStatus = CommandSuccess::instance();
  }
  catch (cvc5::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.what());
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

void GetProofCommand::printResult(cvc5::Solver* solver, std::ostream& out) const
{
  out << d_result;
}

std::string GetProofCommand::getCommandName() const { return "get-proof"; }

void GetProofCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdGetProof(out, d_component);
}

/* -------------------------------------------------------------------------- */
/* class GetInstantiationsCommand                                             */
/* -------------------------------------------------------------------------- */

GetInstantiationsCommand::GetInstantiationsCommand() : d_solver(nullptr) {}
bool GetInstantiationsCommand::isEnabled(cvc5::Solver* solver,
                                         const cvc5::Result& res)
{
  return (res.isSat()
          || (res.isUnknown()
              && res.getUnknownExplanation()
                     == cvc5::UnknownExplanation::INCOMPLETE))
         || res.isUnsat();
}
void GetInstantiationsCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    d_solver = solver;
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

void GetInstantiationsCommand::printResult(cvc5::Solver* solver,
                                           std::ostream& out) const
{
  out << d_solver->getInstantiations();
}

std::string GetInstantiationsCommand::getCommandName() const
{
  return "get-instantiations";
}

void GetInstantiationsCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdGetInstantiations(out);
}

/* -------------------------------------------------------------------------- */
/* class GetInterpolCommand                                                   */
/* -------------------------------------------------------------------------- */

GetInterpolantCommand::GetInterpolantCommand(const std::string& name, Term conj)
    : d_name(name), d_conj(conj), d_sygus_grammar(nullptr)
{
}
GetInterpolantCommand::GetInterpolantCommand(const std::string& name,
                                             Term conj,
                                             Grammar* g)
    : d_name(name), d_conj(conj), d_sygus_grammar(g)
{
}

Term GetInterpolantCommand::getConjecture() const { return d_conj; }

const Grammar* GetInterpolantCommand::getGrammar() const
{
  return d_sygus_grammar;
}

Term GetInterpolantCommand::getResult() const { return d_result; }

void GetInterpolantCommand::invoke(Solver* solver, SymManager* sm)
{
  try
  {
    // we must remember the name of the interpolant, in case
    // get-interpolant-next is called later.
    sm->setLastSynthName(d_name);
    if (d_sygus_grammar == nullptr)
    {
      d_result = solver->getInterpolant(d_conj);
    }
    else
    {
      d_result = solver->getInterpolant(d_conj, *d_sygus_grammar);
    }
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

void GetInterpolantCommand::printResult(cvc5::Solver* solver,
                                        std::ostream& out) const
{
  if (!d_result.isNull())
  {
    out << "(define-fun " << d_name << " () Bool " << d_result << ")"
        << std::endl;
  }
  else
  {
    out << "fail" << std::endl;
  }
}

std::string GetInterpolantCommand::getCommandName() const
{
  return "get-interpolant";
}

void GetInterpolantCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdGetInterpol(
      out, d_name, termToNode(d_conj), grammarToTypeNode(d_sygus_grammar));
}

/* -------------------------------------------------------------------------- */
/* class GetInterpolNextCommand */
/* -------------------------------------------------------------------------- */

GetInterpolantNextCommand::GetInterpolantNextCommand() {}

Term GetInterpolantNextCommand::getResult() const { return d_result; }

void GetInterpolantNextCommand::invoke(Solver* solver, SymManager* sm)
{
  try
  {
    // Get the name of the interpolant from the symbol manager
    d_name = sm->getLastSynthName();
    d_result = solver->getInterpolantNext();
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

void GetInterpolantNextCommand::printResult(cvc5::Solver* solver,
                                            std::ostream& out) const
{
  if (!d_result.isNull())
  {
    out << "(define-fun " << d_name << " () Bool " << d_result << ")"
        << std::endl;
  }
  else
  {
    out << "fail" << std::endl;
  }
}

std::string GetInterpolantNextCommand::getCommandName() const
{
  return "get-interpolant-next";
}

void GetInterpolantNextCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdGetInterpolNext(out);
}

/* -------------------------------------------------------------------------- */
/* class GetAbductCommand                                                     */
/* -------------------------------------------------------------------------- */

GetAbductCommand::GetAbductCommand(const std::string& name, cvc5::Term conj)
    : d_name(name), d_conj(conj), d_sygus_grammar(nullptr)
{
}
GetAbductCommand::GetAbductCommand(const std::string& name,
                                   cvc5::Term conj,
                                   cvc5::Grammar* g)
    : d_name(name), d_conj(conj), d_sygus_grammar(g)
{
}

cvc5::Term GetAbductCommand::getConjecture() const { return d_conj; }

const cvc5::Grammar* GetAbductCommand::getGrammar() const
{
  return d_sygus_grammar;
}

std::string GetAbductCommand::getAbductName() const { return d_name; }
cvc5::Term GetAbductCommand::getResult() const { return d_result; }

void GetAbductCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    // we must remember the name of the abduct, in case get-abduct-next is
    // called later.
    sm->setLastSynthName(d_name);
    if (d_sygus_grammar == nullptr)
    {
      d_result = solver->getAbduct(d_conj);
    }
    else
    {
      d_result = solver->getAbduct(d_conj, *d_sygus_grammar);
    }
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

void GetAbductCommand::printResult(cvc5::Solver* solver,
                                   std::ostream& out) const
{
  if (!d_result.isNull())
  {
    out << "(define-fun " << d_name << " () Bool " << d_result << ")"
        << std::endl;
  }
  else
  {
    out << "fail" << std::endl;
  }
}

std::string GetAbductCommand::getCommandName() const { return "get-abduct"; }

void GetAbductCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdGetAbduct(
      out, d_name, termToNode(d_conj), grammarToTypeNode(d_sygus_grammar));
}

/* -------------------------------------------------------------------------- */
/* class GetAbductNextCommand */
/* -------------------------------------------------------------------------- */

GetAbductNextCommand::GetAbductNextCommand() {}

cvc5::Term GetAbductNextCommand::getResult() const { return d_result; }

void GetAbductNextCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    // Get the name of the abduct from the symbol manager
    d_name = sm->getLastSynthName();
    d_result = solver->getAbductNext();
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

void GetAbductNextCommand::printResult(cvc5::Solver* solver,
                                       std::ostream& out) const
{
  if (!d_result.isNull())
  {
    out << "(define-fun " << d_name << " () Bool " << d_result << ")"
        << std::endl;
  }
  else
  {
    out << "fail" << std::endl;
  }
}

std::string GetAbductNextCommand::getCommandName() const
{
  return "get-abduct-next";
}

void GetAbductNextCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdGetAbductNext(out);
}

/* -------------------------------------------------------------------------- */
/* class GetQuantifierEliminationCommand                                      */
/* -------------------------------------------------------------------------- */

GetQuantifierEliminationCommand::GetQuantifierEliminationCommand()
    : d_term(), d_doFull(true)
{
}
GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(
    const cvc5::Term& term, bool doFull)
    : d_term(term), d_doFull(doFull)
{
}

cvc5::Term GetQuantifierEliminationCommand::getTerm() const { return d_term; }
bool GetQuantifierEliminationCommand::getDoFull() const { return d_doFull; }
void GetQuantifierEliminationCommand::invoke(cvc5::Solver* solver,
                                             SymManager* sm)
{
  try
  {
    if (d_doFull)
    {
      d_result = solver->getQuantifierElimination(d_term);
    }
    else
    {
      d_result = solver->getQuantifierEliminationDisjunct(d_term);
    }
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

cvc5::Term GetQuantifierEliminationCommand::getResult() const
{
  return d_result;
}
void GetQuantifierEliminationCommand::printResult(cvc5::Solver* solver,
                                                  std::ostream& out) const
{
  out << d_result << endl;
}

std::string GetQuantifierEliminationCommand::getCommandName() const
{
  return d_doFull ? "get-qe" : "get-qe-disjunct";
}

void GetQuantifierEliminationCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdGetQuantifierElimination(
      out, termToNode(d_term), d_doFull);
}

/* -------------------------------------------------------------------------- */
/* class GetUnsatAssumptionsCommand                                           */
/* -------------------------------------------------------------------------- */

GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() {}

void GetUnsatAssumptionsCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    d_result = solver->getUnsatAssumptions();
    d_commandStatus = CommandSuccess::instance();
  }
  catch (cvc5::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.what());
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

std::vector<cvc5::Term> GetUnsatAssumptionsCommand::getResult() const
{
  return d_result;
}

void GetUnsatAssumptionsCommand::printResult(cvc5::Solver* solver,
                                             std::ostream& out) const
{
  internal::container_to_stream(out, d_result, "(", ")\n", " ");
}

std::string GetUnsatAssumptionsCommand::getCommandName() const
{
  return "get-unsat-assumptions";
}

void GetUnsatAssumptionsCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdGetUnsatAssumptions(out);
}

/* -------------------------------------------------------------------------- */
/* class GetUnsatCoreCommand                                                  */
/* -------------------------------------------------------------------------- */

GetUnsatCoreCommand::GetUnsatCoreCommand() : d_solver(nullptr), d_sm(nullptr) {}
void GetUnsatCoreCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    d_sm = sm;
    d_solver = solver;
    d_result = solver->getUnsatCore();

    d_commandStatus = CommandSuccess::instance();
  }
  catch (cvc5::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.what());
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

void GetUnsatCoreCommand::printResult(cvc5::Solver* solver,
                                      std::ostream& out) const
{
  if (d_solver->getOption("print-cores-full") == "true")
  {
    // use the assertions
    internal::UnsatCore ucr(termVectorToNodes(d_result));
    ucr.toStream(out);
  }
  else
  {
    // otherwise, use the names
    std::vector<std::string> names;
    d_sm->getExpressionNames(d_result, names, true);
    internal::UnsatCore ucr(names);
    ucr.toStream(out);
  }
}

const std::vector<cvc5::Term>& GetUnsatCoreCommand::getUnsatCore() const
{
  // of course, this will be empty if the command hasn't been invoked
  // yet
  return d_result;
}

std::string GetUnsatCoreCommand::getCommandName() const
{
  return "get-unsat-core";
}

void GetUnsatCoreCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdGetUnsatCore(out);
}

/* -------------------------------------------------------------------------- */
/* class GetUnsatCoreLemmasCommand                                            */
/* -------------------------------------------------------------------------- */

GetUnsatCoreLemmasCommand::GetUnsatCoreLemmasCommand() : d_solver(nullptr) {}
void GetUnsatCoreLemmasCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    d_solver = solver;
    d_result = solver->getUnsatCoreLemmas();

    d_commandStatus = CommandSuccess::instance();
  }
  catch (cvc5::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.what());
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

void GetUnsatCoreLemmasCommand::printResult(cvc5::Solver* solver,
                                            std::ostream& out) const
{
  // use the assertions
  internal::UnsatCore ucr(termVectorToNodes(d_result));
  ucr.toStream(out);
}

std::string GetUnsatCoreLemmasCommand::getCommandName() const
{
  return "get-unsat-core-lemmas";
}

void GetUnsatCoreLemmasCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdGetUnsatCore(out);
}

/* -------------------------------------------------------------------------- */
/* class GetDifficultyCommand */
/* -------------------------------------------------------------------------- */

GetDifficultyCommand::GetDifficultyCommand() : d_sm(nullptr) {}
void GetDifficultyCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    d_sm = sm;
    d_result = solver->getDifficulty();

    d_commandStatus = CommandSuccess::instance();
  }
  catch (cvc5::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.what());
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

void GetDifficultyCommand::printResult(cvc5::Solver* solver,
                                       std::ostream& out) const
{
  out << "(" << std::endl;
  for (const std::pair<const cvc5::Term, cvc5::Term>& d : d_result)
  {
    out << "(";
    // use name if it has one
    std::string name;
    if (d_sm->getExpressionName(d.first, name, true))
    {
      out << name;
    }
    else
    {
      out << d.first;
    }
    out << " " << d.second << ")" << std::endl;
  }
  out << ")" << std::endl;
}

const std::map<cvc5::Term, cvc5::Term>& GetDifficultyCommand::getDifficultyMap()
    const
{
  return d_result;
}

std::string GetDifficultyCommand::getCommandName() const
{
  return "get-difficulty";
}

void GetDifficultyCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdGetDifficulty(out);
}

/* -------------------------------------------------------------------------- */
/* class GetTimeoutCoreCommand */
/* -------------------------------------------------------------------------- */

GetTimeoutCoreCommand::GetTimeoutCoreCommand()
    : d_solver(nullptr), d_sm(nullptr), d_assumptions()
{
}
GetTimeoutCoreCommand::GetTimeoutCoreCommand(
    const std::vector<Term>& assumptions)
    : d_solver(nullptr), d_sm(nullptr), d_assumptions(assumptions)
{
  // providing an empty list of assumptions will make us call getTimeoutCore
  // below instead of getTimeoutCoreAssuming.
  Assert(!d_assumptions.empty());
}
void GetTimeoutCoreCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    d_sm = sm;
    d_solver = solver;
    if (!d_assumptions.empty())
    {
      d_result = solver->getTimeoutCoreAssuming(d_assumptions);
    }
    else
    {
      d_result = solver->getTimeoutCore();
    }
    d_commandStatus = CommandSuccess::instance();
  }
  catch (cvc5::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.what());
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

void GetTimeoutCoreCommand::printResult(cvc5::Solver* solver,
                                        std::ostream& out) const
{
  cvc5::Result res = d_result.first;
  out << res << std::endl;
  if (res.isUnsat()
      || (res.isUnknown()
          && res.getUnknownExplanation() == UnknownExplanation::TIMEOUT))
  {
    if (d_solver->getOption("print-cores-full") == "true")
    {
      // use the assertions
      internal::UnsatCore ucr(termVectorToNodes(d_result.second));
      ucr.toStream(out);
    }
    else
    {
      // otherwise, use the names
      std::vector<std::string> names;
      d_sm->getExpressionNames(d_result.second, names, true);
      internal::UnsatCore ucr(names);
      ucr.toStream(out);
    }
  }
}
cvc5::Result GetTimeoutCoreCommand::getResult() const { return d_result.first; }
const std::vector<cvc5::Term>& GetTimeoutCoreCommand::getTimeoutCore() const
{
  return d_result.second;
}

std::string GetTimeoutCoreCommand::getCommandName() const
{
  return d_assumptions.empty() ? "get-timeout-core"
                               : "get-timeout-core-assuming";
}

void GetTimeoutCoreCommand::toStream(std::ostream& out) const
{
  if (d_assumptions.empty())
  {
    internal::Printer::getPrinter(out)->toStreamCmdGetTimeoutCore(out);
  }
  else
  {
    internal::Printer::getPrinter(out)->toStreamCmdGetTimeoutCoreAssuming(
        out, termVectorToNodes(d_assumptions));
  }
}

/* -------------------------------------------------------------------------- */
/* class GetLearnedLiteralsCommand */
/* -------------------------------------------------------------------------- */

GetLearnedLiteralsCommand::GetLearnedLiteralsCommand(modes::LearnedLitType t)
    : d_type(t)
{
}
void GetLearnedLiteralsCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    d_result = solver->getLearnedLiterals(d_type);

    d_commandStatus = CommandSuccess::instance();
  }
  catch (cvc5::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.what());
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

void GetLearnedLiteralsCommand::printResult(cvc5::Solver* solver,
                                            std::ostream& out) const
{
  out << "(" << std::endl;
  for (const cvc5::Term& lit : d_result)
  {
    out << lit << std::endl;
  }
  out << ")" << std::endl;
}

const std::vector<cvc5::Term>& GetLearnedLiteralsCommand::getLearnedLiterals()
    const
{
  return d_result;
}

std::string GetLearnedLiteralsCommand::getCommandName() const
{
  return "get-learned-literals";
}

void GetLearnedLiteralsCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdGetLearnedLiterals(out,
                                                                    d_type);
}

/* -------------------------------------------------------------------------- */
/* class GetAssertionsCommand                                                 */
/* -------------------------------------------------------------------------- */

GetAssertionsCommand::GetAssertionsCommand() {}
void GetAssertionsCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    stringstream ss;
    const vector<cvc5::Term> v = solver->getAssertions();
    ss << "(\n";
    copy(v.begin(), v.end(), ostream_iterator<cvc5::Term>(ss, "\n"));
    ss << ")\n";
    d_result = ss.str();
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

std::string GetAssertionsCommand::getResult() const { return d_result; }
void GetAssertionsCommand::printResult(cvc5::Solver* solver,
                                       std::ostream& out) const
{
  out << d_result;
}

std::string GetAssertionsCommand::getCommandName() const
{
  return "get-assertions";
}

void GetAssertionsCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdGetAssertions(out);
}

/* -------------------------------------------------------------------------- */
/* class SetBenchmarkLogicCommand                                             */
/* -------------------------------------------------------------------------- */

SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic)
    : d_logic(logic)
{
}

std::string SetBenchmarkLogicCommand::getLogic() const { return d_logic; }
void SetBenchmarkLogicCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    sm->setLogic(d_logic);
    solver->setLogic(d_logic);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

std::string SetBenchmarkLogicCommand::getCommandName() const
{
  return "set-logic";
}

void SetBenchmarkLogicCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdSetBenchmarkLogic(out,
                                                                   d_logic);
}

/* -------------------------------------------------------------------------- */
/* class SetInfoCommand                                                       */
/* -------------------------------------------------------------------------- */

SetInfoCommand::SetInfoCommand(const std::string& flag,
                               const std::string& value)
    : d_flag(flag), d_value(value)
{
}

const std::string& SetInfoCommand::getFlag() const { return d_flag; }
const std::string& SetInfoCommand::getValue() const { return d_value; }
void SetInfoCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    solver->setInfo(d_flag, d_value);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (cvc5::CVC5ApiUnsupportedException&)
  {
    // As per SMT-LIB spec, silently accept unknown set-info keys
    d_commandStatus = CommandSuccess::instance();
  }
  catch (cvc5::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.getMessage());
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

std::string SetInfoCommand::getCommandName() const { return "set-info"; }

void SetInfoCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdSetInfo(out, d_flag, d_value);
}

/* -------------------------------------------------------------------------- */
/* class GetInfoCommand                                                       */
/* -------------------------------------------------------------------------- */

GetInfoCommand::GetInfoCommand(std::string flag) : d_flag(flag) {}
std::string GetInfoCommand::getFlag() const { return d_flag; }
void GetInfoCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    TermManager& tm = solver->getTermManager();
    std::vector<cvc5::Term> v;
    Sort bt = tm.getBooleanSort();
    v.push_back(tm.mkVar(bt, ":" + d_flag));
    v.push_back(tm.mkVar(bt, solver->getInfo(d_flag)));
    d_result = sexprToString(tm.mkTerm(cvc5::Kind::SEXPR, {v}));
    d_commandStatus = CommandSuccess::instance();
  }
  catch (cvc5::CVC5ApiUnsupportedException&)
  {
    d_commandStatus = new CommandUnsupported();
  }
  catch (cvc5::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.getMessage());
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

std::string GetInfoCommand::getResult() const { return d_result; }
void GetInfoCommand::printResult(cvc5::Solver* solver, std::ostream& out) const
{
  if (d_result != "")
  {
    out << d_result << endl;
  }
}

std::string GetInfoCommand::getCommandName() const { return "get-info"; }

void GetInfoCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdGetInfo(out, d_flag);
}

/* -------------------------------------------------------------------------- */
/* class SetOptionCommand                                                     */
/* -------------------------------------------------------------------------- */

SetOptionCommand::SetOptionCommand(const std::string& flag,
                                   const std::string& value)
    : d_flag(flag), d_value(value)
{
}

const std::string& SetOptionCommand::getFlag() const { return d_flag; }
const std::string& SetOptionCommand::getValue() const { return d_value; }
void SetOptionCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    solver->setOption(d_flag, d_value);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (cvc5::CVC5ApiUnsupportedException&)
  {
    d_commandStatus = new CommandUnsupported();
  }
  catch (cvc5::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.getMessage());
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

std::string SetOptionCommand::getCommandName() const { return "set-option"; }

void SetOptionCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdSetOption(
      out, d_flag, d_value);
}

/* -------------------------------------------------------------------------- */
/* class GetOptionCommand                                                     */
/* -------------------------------------------------------------------------- */

GetOptionCommand::GetOptionCommand(std::string flag) : d_flag(flag) {}
std::string GetOptionCommand::getFlag() const { return d_flag; }
void GetOptionCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  try
  {
    d_result = solver->getOption(d_flag);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (cvc5::CVC5ApiUnsupportedException&)
  {
    d_commandStatus = new CommandUnsupported();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

std::string GetOptionCommand::getResult() const { return d_result; }
void GetOptionCommand::printResult(cvc5::Solver* solver,
                                   std::ostream& out) const
{
  if (d_result != "")
  {
    out << d_result << endl;
  }
}

std::string GetOptionCommand::getCommandName() const { return "get-option"; }

void GetOptionCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdGetOption(out, d_flag);
}

/* -------------------------------------------------------------------------- */
/* class DatatypeDeclarationCommand                                           */
/* -------------------------------------------------------------------------- */

DatatypeDeclarationCommand::DatatypeDeclarationCommand(
    const cvc5::Sort& datatype)
    : d_datatypes()
{
  d_datatypes.push_back(datatype);
}

DatatypeDeclarationCommand::DatatypeDeclarationCommand(
    const std::vector<cvc5::Sort>& datatypes)
    : d_datatypes(datatypes)
{
}

const std::vector<cvc5::Sort>& DatatypeDeclarationCommand::getDatatypes() const
{
  return d_datatypes;
}

void DatatypeDeclarationCommand::invoke(cvc5::Solver* solver, SymManager* sm)
{
  // Implement the bindings. We bind tester names is-C if strict parsing is
  // disabled.
  bool bindTesters = solver->getOption("strict-parsing") != "true";
  if (!sm->bindMutualDatatypeTypes(d_datatypes, bindTesters))
  {
    // this should generally never happen since we look ahead to check whether
    // binding will succeed in Parser::mkMutualDatatypeTypes.
    std::stringstream ss;
    ss << "Failed to implement bindings for symbols in definition of datatype "
          "in block containing "
       << d_datatypes[0];
    d_commandStatus = new CommandFailure(ss.str());
  }
  else
  {
    d_commandStatus = CommandSuccess::instance();
  }
}

std::string DatatypeDeclarationCommand::getCommandName() const
{
  return "declare-datatypes";
}

void DatatypeDeclarationCommand::toStream(std::ostream& out) const
{
  internal::Printer::getPrinter(out)->toStreamCmdDatatypeDeclaration(
      out, sortVectorToTypeNodes(d_datatypes));
}

}  // namespace cvc5::parser
